COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	provin[f85,jmc]		Proving programs correct
C00005 ENDMK
C⊗;
provin[f85,jmc]		Proving programs correct

Debug Proofs Instead of Programs

	I haven't given this paper since 1962.

	A computer program is a mathematical object, and its properties
are mathematical facts.  Determining whether a program meets its
specifications by debugging, i.e. trying examples, is like verifying
a mathematical theorem by substituting numbers.  The fact that programs
are debugged is a mathematical disgrace.

	Moreover, it is intrinsic to the notion of proof that it can
be verified by computer.  Therefore, debugging should be replaced by
preparing a proof that a program meets its specifications and checking
this proof by computer.  If the attempt to prove the correctness statement
fails, the statement may be false.  We repair the proof, which may
involve repairing the program and try again.  Thus debugging programs
is to be replaced by debugging proofs.  The difference is that a
proof can be finally debugged, while no feasible collection of
correct runs conclusively verifies that a program is correct (except
in a few unimportant cases or when only bugs from a certain subset
are considered).

	All this was said in (McCarthy 1962), and the object of the
present paper is to review the situation.

	First of all, the whole idea was attacked in (de Milo, Lipton
and Perlis 197x), and it needs to be refined a bit and defended against
that attack.